Small refactoring of partition information #219
Conversation
blishko
force-pushed
the
partition-refactor
branch
from
4ec9391
to
b6b90d6
Compare
This cleans up Cnfizer a bit, because it does not need to know about the partitioning anymore.
blishko
force-pushed
the
partition-refactor
branch
from
b6b90d6
to
6806db7
Compare
There was a problem hiding this comment.
This looks good!
I'm thinking about the interface though. Could we pass the partitionIndex as an argument to the newSMTClause methods in {Core,Simp}SMTSolver, and therefore also at insertFormula in MainSolver? I think it would be good not to rely on the state in the SMT solver. For instance the partitions of true and false are not very explicit in the current implementation, and the partitions of the satelite-simplified clauses (which we hopefully are not doing) would be explicit. This was probably an issue in the old code already, but could be good to discuss at this PR. I made quickly the change on my local working directory, and could commit it here if you want.
| @@ -1044,6 +1035,12 @@ void CoreSMTSolver::finalizeProof(CRef finalConflict) { | |||
| proof->endChain(CRef_Undef); | |||
| } | |||
|
|
|||
| void CoreSMTSolver::setPartition(std::size_t partitionIndex) { | |||
| if (proof) { | |||
There was a problem hiding this comment.
Change to logsProofForInterpolation()?
| { | ||
| assert(decisionLevel() == 0); | ||
| inOutCRefs = {CRef_Undef, CRef_Undef}; | ||
| if (!isOK()) { return false; } | ||
| bool logsProofForInterpolation = this->logsProofForInterpolation(); |
There was a problem hiding this comment.
This old code seems a little redundant. Maybe we could fix it on this commit as well.
|
I agree that the interface is not entirely clear. For some reason I don't like the idea of explicitly passing the index in the If you have some proposal, maybe commit to a separate branch and send a link? Now I feel that it might be good to change the interpolation interface to not use |
This PR proposes moving the partition information of clauses directly to the proof structure, as this is needed only for building resolution proof for interpolation.
This change allows to clean up the interface of adding clauses to the SAT solver and removes the dependency of
CnfizeronPartitionManager.